from z3 import *


s = Solver()
A = DeclareSort("A")
R = Function("R", A, A, BoolSort())
x, y, z = Consts("x y z", A)
s.add(ForAll([x], R(x, x)))
s.add(ForAll([x, y], Implies(And(R(x, y), R(y, x)), x == y)))
s.add(ForAll([x, y, z], Implies(And(R(x, y), R(y, z)), R(x, z))))
# and other assertions using R

R = PartialOrder(A, 0)
s.Add(ForAll([x], R(x, x)))
s.Add(ForAll([x,y], Implies(And(R(x, y), R(y, x)), x == y)))
s.Add(ForAll([x,y,z], Implies(And(R(x, y), R(y, z)), R(x, z))))
s.Add(ForAll([x,y], Or(R(x, y), R(y, x))))

# use instead:
R = LinearOrder(A, 0)
s.Add(ForAll([x], R(x, x)))
s.Add(ForAll([x,y], Implies(And(R(x, y), R(y, x)), x == y)))
s.Add(ForAll([x,y,z], Implies(And(R(x, y), R(y, z)), R(x, z))))
s.Add(ForAll([x,y,z], Implies(And(R(x, y), R(x, z)), Or(R(y, z), R(z, y)))))

# use instead:
R = TreeOrder(A, 0)

s.Add(ForAll([x], R(x, x)))
s.Add(ForAll([x,y], Implies(And(R(x, y), R(y, x)), x == y)))
s.Add(ForAll([x,y,z], Implies(And(R(x, y), R(y, z)), R(x, z))))
s.Add(ForAll([x,y,z], Implies(And(R(x, y), R(x, z)), Or(R(y, z), R(z, y)))))
s.Add(ForAll([x,y,z], Implies(And(R(y, x), R(z, x)), Or(R(y, z), R(z, y)))))

# use instead:
R = PiecewiseLinearOrder(A, 0)